(set-option :incremental false)
(set-info :status unsat)
(set-logic QF_AUF)
(declare-sort Index 0)
(declare-sort Element 0)
(declare-fun v3 () Index)
(declare-fun v4 () Index)
(declare-fun v2 () Index)
(check-sat-assuming ( (let ((_let_0 (distinct v2 v3))) (and (xor true (= v4 v3)) (ite (distinct v4 (ite _let_0 (ite _let_0 v3 v4) v3)) false true))) ))
